package preprocessor.absorption.extended;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import option.InitParam;
import preprocessor.Simplification;

import reasoner.KBReason;
import utils.exception.CoreReasoningException;

import kb.TBox;

import entities.Individual;
import entities.assertion.ConceptAssertion;
import entities.concept.Concept;
import entities.concept.Nominal;
import entities.concept.PConcept;
import entities.role.Role;

public class OptimizedRestrictions {
	protected static Map<Individual, HashMap<Role, HashSet<Individual>>> allRAs = 
			new HashMap<Individual, HashMap<Role, HashSet<Individual>>>();
	protected static Map<Role, Map<Concept, Set<Concept>>> normalizedUniversals = 
			new HashMap<Role, Map<Concept, Set<Concept>>>();
	protected static Map<Concept, Set<Individual>> realizedInds = 
			new HashMap<Concept, Set<Individual>>();
	protected static Map<Role, Map<Concept, Set<Concept>>> normalizedExists = 
			new HashMap<Role, Map<Concept, Set<Concept>>>();
	public static long lookup = 0;
	public static long realizedHit = 0;

	protected static boolean verbose = false;
	public static boolean OptimizeEx = InitParam
	.getBooleanProperty("reasoning.guarding.exist.precomputed");
	public static boolean OptimizeUR = InitParam
	.getBooleanProperty("reasoning.guarding.universal.precomputed");
	private static boolean checkNegation = true;
	
	
	public static void optimize(TBox tb){
		try{
			
			if(OptimizeEx){
				OptimizedExistentials.optimizeEX(tb);
			}
			if(OptimizeUR){
				OptimizedUniversals.optimizeUR(tb);
			}
		}catch(Exception ex){
			ex.printStackTrace();
		}
		
	}
	
	protected static boolean isInstance(Individual a, Concept A, boolean logical, TBox tb) 
			throws CoreReasoningException{
		if(A.isTop()){
			return true;
		}
		if(A.isBot()){
			return false;
		}
		if(checkNegation){
			Concept NA = Simplification.NNF(A, true);
			if(hasRealized(NA, a)){
				realizedHit ++;
				return false;
			}
		}
		if(hasRealized(A, a)){
			realizedHit ++;
			return true;
		}
		if(syntacticCheck(a, A, tb)){
			return true;
		}
		if(logical && tb != null){
			boolean log = new KBReason().
					logicConsequenceGuarded(null, new ConceptAssertion(a,A), tb);
			if(log){
				addRealizedInd(A, a);
			}
			return log;
		}
		return false;
	}
	
	private static boolean syntacticCheck(Individual ia, Concept A, TBox tb){
		Nominal na = Nominal.getNominal(ia.getName(), false);
		PConcept defa = PConcept.newGuardPConcept(ia);
		Concept entry = tb.getSpecialBinaryClass().getEntry(na, defa);
		if(entry == null){
			return false;
		}
		for(Concept and:Concept.reduceToConjuncts(entry)){
			if(and.equals(A)){
				lookup++;
				return true;
			}
		}
		return false;
	}
	public static void clearAllCache(){
		allRAs.clear();
		normalizedUniversals.clear();
		realizedInds.clear();
		OptimizedUniversals.clearAll();
	}
	
	protected static boolean hasRealized(Concept c, Individual a) {
		if (realizedInds.containsKey(c)) {
			return realizedInds.get(c).contains(a);
		}
		return false;
	}

	protected static void addRealizedInd(Concept c, Individual n) {
		Set<Individual> ns = realizedInds.get(c);
		if (ns == null) {
			ns = new HashSet<Individual>();
		}
		ns.add(n);
		realizedInds.put(c, ns);
	}
}
